Inference at * 2 
Iof proof for Lemma absval elim:



1. P : 
2. x:. P(x)
3. x : 
  P(|x|) 

latex

 by Unfold `absval` 0 

latex

 1: 

 1:   P(if 0 z x then x else -x fi )
 .

Definitions

|i|